r, s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s)) 

latex

Definitions	a = b mod m, P  Q, CoPrime(a,b), x:A. B(x), t  T, , P  Q, P & Q, x:A. B(x), Prop, b | a, T, True
Lemmas	divides reflexivity, divisor of mul, divisor of minus, true wf, squash wf, divides wf, coprime bezout id, nat plus wf, coprime wf